Library isogonal_conjugate
Require Export PointsType.
Require Import incidence.
Require Import circumcircle.
Open Scope R_scope.
Section Triangle.
Context `{M:triangle_theory}.
Definition isogonal_conjugate P :=
match P with
cTriple p q r ⇒
cTriple (1/p) (1/q) (1/r)
end.
Require Import incidence.
Require Import circumcircle.
Open Scope R_scope.
Section Triangle.
Context `{M:triangle_theory}.
Definition isogonal_conjugate P :=
match P with
cTriple p q r ⇒
cTriple (1/p) (1/q) (1/r)
end.
The isogonal conjugate of a point on the circumcircle is a point at infinity
Lemma isogonal_circumcircle_property :
∀ P,
is_not_on_sidelines P →
is_on_circumcircle P →
is_at_infinity (isogonal_conjugate P).
Proof.
intros.
destruct P.
simpl in ×.
decompose [and] H.
intros.
assert ((a × Y × Z + b × Z × X + c × X × Y) / (X×Y×Z) = 0).
rewrite H0.
field;intuition.
rewrite <- H2.
field;intuition.
Qed.
End Triangle.